|
The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix〔(D. Knuth, "The Genesis of Attribute Grammars" )〕) is a semi-decision〔, p. 55〕 algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra. Buchberger's algorithm for computing Gröbner bases is a very similar algorithm. Although developed independently, it may also be seen as the instantiation of Knuth–Bendix algorithm in the theory of polynomial rings. ==Introduction== For a set ''E'' of equations, its deductive closure () is the set of all equations that can be derived by applying equations from ''E'' in any order. Formally, ''E'' is considered a binary relation, () is its rewrite closure, and () is the equivalence closure of (). For a set ''R'' of rewrite rules, its deductive closure ( ∘ ) is the set of all equations than can be confirmed by applying rules from ''R'' left-to-right to both sides until they are literally equal. Formally, ''R'' is again viewed as binary relation, () is its rewrite closure, () is its converse, and ( ∘ ) is the relation composition of their reflexive transitive closures ( and ). For example, if are the group axioms, the derivation chain : demonstrates that ''a''−1⋅(''a''⋅''b'') ''b'' is a member of ''Es deductive closure. If is a "rewrite rule" version of ''E'', the derivation chains : demonstrate that (''a''−1⋅''a'')⋅''b'' ∘ ''b''⋅1 is a member of ''Rs deductive closure. However, there is no way to derive ''a''−1⋅(''a''⋅''b'') ∘ ''b'' similar to above, since a right-to-left application of the rule is not allowed. The Knuth–Bendix algorithm takes a set ''E'' of equations between terms, and a reduction ordering (>) on the set of all terms, and attempts to construct a confluent and terminating term rewriting system ''R'' that has the same deductive closure as ''E''. While proving consequences from ''E'' often requires human intuition, proving consequences from ''R'' does not. For more details, see Confluence (abstract rewriting)#Motivating examples, which gives an example proof from group theory, performed both using ''E'' and using ''R''. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Knuth–Bendix completion algorithm」の詳細全文を読む スポンサード リンク
|